시퀀트 계산

시퀀트 계산(sequent calculus)은 연역 체계의 일종으로, 게르하르트 겐첸이 1934년 논문 「논리적 추론에 관한 연구」에서 자연 연역 체계와 함께 발표하였다. 시퀀트 계산에서는 시퀀트라는 수학적 객체를 조작한다. 따라서 조작 방식에 따라 다양한 시퀀트 계산이 존재한다. 이 문서는 특히, (i) 최초로 제시된 겐첸의 체계 \(\textbf{LK}\)와 \(\textbf{LJ}\)(=클레이니의 \(\textbf{G}_{1}\)), (ii) 그리고 클레이니의 \(\textbf{G}_{3}\)을 다룬다.

시퀀트

정의: 시퀀트는 공식의 두 나열(sequence) \(\Gamma, \Delta\)의 순서쌍 \((\Gamma, \Delta)\)이다.

용어법: 시퀀트에 대해 다음 명칭이 통용된다. 한 시퀀트 \((\Gamma,\Delta)\)에 대해,

1. 시퀀트 \((\Gamma, \Delta)\)를 \((\Gamma \Rightarrow \Delta)\)라고 쓴다. 문맥에 따라 괄호는 생략할 수 있다.

2. \(\Gamma\)를 시퀀트의 전건(antecedent), \(\Delta\)를 시퀀트의 후건(succedent)이라 부른다.

3. 나열의 접합(concatenation) 연산을 쉼표(\(,\))로 표기하고, 개별 공식을 한 원소 나열로 간주한다. 따라서 \((\Gamma,\varphi,\Delta\Rightarrow \Lambda,\psi,\Theta)\) 꼴 표기가 가능하다.

4. 시퀀트의 전건이나 후건이 빈 나열일 경우, 공백으로 표기한다(\((\Rightarrow \Delta)\) 또는 \((\Gamma \Rightarrow)\)).

시퀀트 \(\varphi_1,\cdots,\varphi_n\Rightarrow\psi_1,\cdots,\psi_m\)의 의미는, 문장 \((\varphi_1\wedge\cdots\wedge\varphi_n)\rightarrow (\psi_1\vee\cdots\vee\psi_m)\)의 의미와 같다고 이해할 수 있다. 따라서, 한 시퀀트가 옳다(correct)는 것은 대응하는 문장이 같은 조건 하에서 참임과 같다고 이해할 수 있다.

시퀀트 계산 개요

논리 체계는 가정 공식들로부터 하나의 결론 공식을 유도한다. 증명은 유도과정의 명세다. 그래서 증명은 다수의 단말 노드(가정)로부터 루트 노드(결론)를 향해 수렴하는 트리 구조를 갖는다. 시퀀트 계산은 증명 트리의 공식 자리에 시퀀트를 놓는다. 그래서 마찬가지로 트리 구조를 갖는다. \(n\)개의 가정 시퀀트 \(\Gamma_1 \Rightarrow \Delta_1, \cdots, \Gamma_n \Rightarrow \Delta_n\)로부터 결론 \(\Gamma'\Rightarrow \Delta'\)를 도출하는 시퀀트 계산 규칙이 사용될 때, 다음으로 표기한다. \[ \begin{prooftree} \AxiomC{ $\Gamma_1\Rightarrow\Delta_1$ } \AxiomC{ $\cdots$ } \AxiomC{ $\Gamma_n\Rightarrow\Delta_n$ } \RightLabel{(규칙명)} \TrinaryInfC{ $\Gamma'\Rightarrow\Delta'$ } \end{prooftree} \]

시퀀트 계산의 추론 규칙은 귀결 관계의 전건과 후건의 조작으로 이해할 수 있다. 편의상 후건이 문장 하나 뿐이라고 생각하자. 그러면 시퀀트 \((\Gamma \Rightarrow \varphi)\)를 귀결 관계로 이해할 수 있다.

증명구조의 성격을 이해하면, 문장 대신 시퀀트를 조작 대상으로 간주하는 기본 발상을 이해할 수 있다. 이를 자연 연역의 함축 도입 규칙(\(\rightarrow^{+}\))의 사례를 통해 알아보자. \[ \begin{prooftree} \AxiomC{ $[A]^{1}$ } \AxiomC{ $\Gamma_1$ } \noLine \UnaryInfC{ $\vdots$ } \BinaryInfC{ $\vdots$ } \AxiomC{ $[A]^1$ } \AxiomC{ $\Gamma_2$ } \noLine \UnaryInfC{ $\vdots$ } \AxiomC{ $[A]^1$ } \BinaryInfC{ $\vdots$ } \BinaryInfC{ $\vdots$ } \BinaryInfC{ $\vdots$ } \UnaryInfC{ $B$ } \RightLabel{ $\rightarrow^{+}$, 1 } \UnaryInfC{ $A\rightarrow B$ } \end{prooftree} \] 이 증명 트리에서 \(A\rightarrow B\)를 도출해내기 위해, 단말에 있는 \(A\)에 첨수 \(1\)로 마킹해야 한다(\([A]^{1}\)). 즉, 개별 문장을 증명하려 할 때마다, \(\rightarrow^{+}\) 규칙이 사용되면, 증명구조 전체를 역순으로 탐색하여, 맥락이 갖는 정보를 변경(\(A\)에 \(1\)로 마킹)한다. 그러므로, \(\rightarrow^{+}\) 규칙은 맥락 의존적(context-sensitive)인 규칙이다. 이 규칙은 만약 맥락이 존재한다면 추론을 통해 맥락을 변형한다. 반면 시퀀트 계산은 맥락 의존성을 전건에 명세함으로써, 증명 도중 맥락이 어떻게 변형되었는지를 한 시퀀트 내에서 표현할 수 있다. 그래서, 규칙 \(\rightarrow^{+}\)를 사용하는 자연 연역 증명을 \(\textbf{LK}\) 증명의 \(\rightarrow_{R}\) 규칙의 사용 사례로 간주할 수 있다. \[ \begin{prooftree} \AxiomC{ $\Gamma_1, \Gamma_2, A\Rightarrow B$ } \RightLabel{ $\rightarrow_{R}$ } \UnaryInfC{ $\Gamma_1, \Gamma_2\Rightarrow A\rightarrow B$ } \end{prooftree} \] 이 시퀀트 계산 규칙에서, 우리가 보이는 것은 \(A\rightarrow B\)를 전제로부터 증명할 수 있음을 보이는 것이다. 그런데, 자연 연역 증명에서와 달리, 증명의 제반 맥락에 대한 정보가 시퀀트의 전건에 모두 속해 있으므로, 이 계산법에서는 시퀀트 증명 구조 전체를 기억하지 않고, 개별 시퀀트를 조작하거나 병합하는 방식으로 풀 수 있도록 증명 문제를 변형한다.

한 가지 더 주목할 점은, 시퀀트 계산에서, 가정에서 결론을 향해 추론이 이루어질 때, 몇 가지 규칙을 제외하면, 나머지 규칙은 모두 가정 시퀀트들에 나타나는 공식들과 결론 시퀀트에 나타나는 공식의 부분공식을 모두 공유한다. (방금 든 \(\rightarrow_{R}\)의 예시에서, 규칙 위쪽 시퀀트와 규칙 아래쪽 시퀀트는 모두, 공식 \(\Gamma_1, \Gamma_2, A, B\)를 공유한다.) 위 시퀀트의 각 공식에 나타나는 연결사들은, 아래 시퀀트를 산출하기 위해 어떤 규칙을 사용해야 하는지 결정하고, 역도 성립한다. 따라서, 시퀀트 증명 트리의 위쪽이 일부 비어있을 때, 아래쪽을 사용하여 가정을 재구성할 수 있다. 이러한 방식의 증명을 시퀀트 계산에서의 분석적 증명(analytic proof)이라고 부른다. 반면 다른 규칙은 분석적 증명에 사용하기에 적합하지 않다. 예를 들면 다음 규칙을 보자. \[ \begin{prooftree} \AxiomC{ $\Gamma_1\Rightarrow \Delta_1, B$ } \AxiomC{ $B, \Gamma_2\Rightarrow \Delta_2$ } \RightLabel{ cut } \BinaryInfC{ $\Gamma_1, \Gamma_2\Rightarrow \Delta_1,\Delta_2$ } \end{prooftree} \]

편의상 \((\Delta_1, \Delta_2)\)가 한 문장 \(\varphi\)라고 하면 이해가 쉽다. 이 규칙에서 위쪽 두 시퀀트에 모두 나타나는 공식 \(B\)는 아래 시퀀트에서 사라진다. 그래서 만약 아래 시퀀트가 먼저 주어졌을 때, 위 시퀀트를 역순으로 알아내야 한다면, \(B\)가 어떤 공식인지 아래 시퀀트만 봐서는 알 방법이 없다. 이 규칙을 사용해야 하는 증명에 대해서는, 아래 시퀀트로부터 효과적인 역순 재구성은 불가능하다(문장은 무한하므로). 그러므로, 분석적 규칙만 사용해 모든 시퀀트를 증명할 수 있는지를 효과적인 증명 체계를 구성할 때 확인해야 한다. 겐첸에 따르면, 상단의 컷 규칙은 증명능력에 효과를 미치지 않는다. 즉, 시퀀트 계산에서 컷 규칙은 부수적이다. 이것이 겐첸이 시퀀트 계산 체계 \(\textbf{LK}\)에 대해 보인 자름-제거 정리이다.

시스템 \(\textbf{LK}\)

시스템 \(\textbf{LK}\)는 다음 규칙으로 이루어진다. 모든 문장 \(A, B, \cdots\)와 문장의 나열 \(\Gamma, \Delta, \Lambda, \Theta, \cdots\)에 대해,

1. 공리: \[ \begin{prooftree} \AxiomC{} \UnaryInfC{ $A\Rightarrow A$ } \end{prooftree} \]

   첨언: 공리 규칙에는 임의의 문장 \(A\) 대신 명제 변항 \(p\)를 대신 쓰는 경우가 있다. 이 경우, 더 일반적인 경우인 \((A\Rightarrow A)\)의 증명 가능성은 \(\textbf{LK}\)에서는 귀납법으로 보일 수 있다.

2. 세 그룹의 구조 규칙―약화(Weakening), 축약(Contraction), 교환(Exchange): \[ \begin{prooftree} \AxiomC{$\Gamma\Rightarrow \Delta$} \RightLabel{$W_{L}$} \UnaryInfC{ $A, \Gamma\Rightarrow \Delta$ } \end{prooftree} \mkern4em \begin{prooftree} \AxiomC{$\Gamma\Rightarrow \Delta$} \RightLabel{$W_{R}$} \UnaryInfC{ $\Gamma\Rightarrow \Delta, A$ } \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$A, A, \Gamma\Rightarrow \Delta$} \RightLabel{$C_{L}$} \UnaryInfC{ $A, \Gamma\Rightarrow \Delta$ } \end{prooftree} \mkern4em \begin{prooftree} \AxiomC{$\Gamma\Rightarrow \Delta, A, A$} \RightLabel{$C_{R}$} \UnaryInfC{ $\Gamma\Rightarrow \Delta, A$ } \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma, A, B, \Delta\Rightarrow \Theta$} \RightLabel{$E_{L}$} \UnaryInfC{ $\Gamma, B, A, \Delta\Rightarrow \Theta$ } \end{prooftree} \mkern4em\begin{prooftree} \AxiomC{$\Gamma \Rightarrow \Delta,A,B, \Theta$} \RightLabel{$E_{R}$} \UnaryInfC{ $\Gamma\Rightarrow\Delta, B, A, \Theta$ } \end{prooftree} \]

3. 컷: \[ \begin{prooftree} \AxiomC{ $\Gamma\Rightarrow \Delta, B$ } \AxiomC{ $B, \Lambda\Rightarrow \Theta$ } \RightLabel{ cut } \BinaryInfC{ $\Gamma, \Lambda\Rightarrow \Delta,\Theta$ } \end{prooftree} \]

4. 논리연결사 규칙: \[ \begin{prooftree} \AxiomC{$A,\Gamma\Rightarrow \Delta$} \RightLabel{$\wedge_{L1}$} \UnaryInfC{ $(A\wedge B), \Gamma\Rightarrow \Delta$ } \end{prooftree} \mkern4em \begin{prooftree} \AxiomC{$B,\Gamma\Rightarrow \Delta$} \RightLabel{$\wedge_{L2}$} \UnaryInfC{ $(A\wedge B), \Gamma\Rightarrow \Delta$ } \end{prooftree} \] \[ \begin{prooftree} \AxiomC{ $\Gamma\Rightarrow \Delta, A$ } \AxiomC{ $\Gamma\Rightarrow \Delta, B$ } \RightLabel{ $\wedge_{R}$ } \BinaryInfC{ $\Gamma\Rightarrow \Delta, (A\wedge B)$ } \end{prooftree} \] \[ \begin{prooftree} \AxiomC{ $A, \Gamma\Rightarrow \Delta$ } \AxiomC{ $B, \Gamma\Rightarrow \Delta$ } \RightLabel{ $\vee_{L}$ } \BinaryInfC{ $(A\lor B), \Gamma\Rightarrow \Delta$ } \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma\Rightarrow \Delta, A$} \RightLabel{$\vee_{R1}$} \UnaryInfC{ $\Gamma\Rightarrow \Delta, (A\vee B)$ } \end{prooftree} \mkern4em \begin{prooftree} \AxiomC{$\Gamma\Rightarrow \Delta, B$} \RightLabel{$\vee_{R2}$} \UnaryInfC{ $\Gamma\Rightarrow \Delta, (A\vee B)$ } \end{prooftree} \] \[ \begin{prooftree} \AxiomC{ $\Gamma\Rightarrow \Delta, A$ } \AxiomC{ $B, \Lambda\Rightarrow \Theta$ } \RightLabel{ $\rightarrow_{L}$ } \BinaryInfC{ $(A\rightarrow B), \Gamma, \Lambda\Rightarrow \Delta,\Theta$ } \end{prooftree} \kern4em \begin{prooftree} \AxiomC{ $\Gamma, A\Rightarrow B,\Delta$ } \RightLabel{ $\rightarrow_{R}$ } \UnaryInfC{ $\Gamma\Rightarrow (A\rightarrow B),\Delta$ } \end{prooftree} \] \[ \begin{prooftree} \AxiomC{ $\Gamma\Rightarrow A, \Delta$ } \RightLabel{ $\neg{L}$ } \UnaryInfC{ $\Gamma, \neg A\Rightarrow \Delta$ } \end{prooftree} \kern 4em \begin{prooftree} \AxiomC{ $\Gamma, A\Rightarrow \Delta$ } \RightLabel{ $\neg{R}$ } \UnaryInfC{ $\Gamma\Rightarrow \neg A, \Delta$ } \end{prooftree} \] \[ \begin{prooftree} \AxiomC{ $ A[\tau/x], \Gamma\Rightarrow \Delta$ } \RightLabel{ $\forall_{L}$ } \UnaryInfC{ $\forall x A, \Gamma \Rightarrow \Delta$ } \end{prooftree} \kern 4em \begin{prooftree} \AxiomC{ $\Gamma\Rightarrow \Delta, A[y/x]$ } \RightLabel{ $\forall_{R}$ } \UnaryInfC{ $\Gamma\Rightarrow \Delta, \forall xA$ } \end{prooftree} \] \[ \begin{prooftree} \AxiomC{ $ A[y/x], \Gamma\Rightarrow \Delta$ } \RightLabel{ $\exists_{L}$ } \UnaryInfC{ $\exists x A, \Gamma \Rightarrow \Delta$ } \end{prooftree} \kern 4em \begin{prooftree} \AxiomC{ $\Gamma\Rightarrow \Delta, A[\tau/x]$ } \RightLabel{ $\exists_{R}$ } \UnaryInfC{ $\Gamma\Rightarrow \Delta, \exists xA$ } \end{prooftree} \]

용어법: 개별 시퀀트 계산 규칙에서,

1. 가로선 밑의 시퀀트를 아래 시퀀트(lower sequent)라고 부르고, 위의 시퀀트를 위 시퀀트(upper sequent)라 부른다.
2. 위 시퀀트에 나타나지 않는 공식이 규칙을 사용함으로써 아래 시퀀트에 새로 나타나면, 그 공식을 규칙의 주공식(principal formula)이라 부른다.
3. 주공식의 진부분공식이 위 시퀀트에 나타나는 것이 규칙의 성립 조건이면, 그 진부분공식들을 변공식(side formula)이라 부른다.
4. 위 시퀀트에 나타난 공식이 규칙을 사용함으로써 아래 시퀀트에서는 제거된다면, 그 공식을 규칙의 컷 공식(cut formula)이라 부른다.
5. 규칙을 통해 변경되지 않고 복사되는 공식을 여분공식(extra formula)이라 부른다.

예를 들어, \(\rightarrow_{L}\) 규칙에서, (i) \((A\rightarrow B)\)는 규칙의 주공식이다. (ii) \(A, B\)는 규칙의 변공식이다. \(\Gamma, \Delta, \Lambda, \Theta\)에 나타나는 문장은 여분공식이다.

또한, \(\forall, \exists\) 규칙의 경우, \(\tau\)는 \(A\)에 나타난 \(x\)에 자유롭게 치환할 수 있는(term \(\tau\) is free/substitutable for \(x\) in \(A\)) 항이어야만 하고, \(y\)는 \(A\)에만 고유한 변수(eigenvariable)여야 한다. 자유롭게 치환할 수 있음은 곧, \(A\)의 구속변수(bound variable)가 \(\tau\)에 나타나지 않음을 의미한다. 고유 변수임은 곧, 규칙의 아래 시퀀트에 \(y\)가 나타나지 않음을 의미한다. (즉, \(y\)는 \(A\)에만 나타나야 하고, \(\Gamma,\Delta\) 그리고 주공식에는 나타나면 안 된다.)

논리연결사 규칙의 명칭은 연결사를 시퀀트의 전건(\(L\))에 도입하는가 후건(\(R\))에 도입하는가에 따라 결정된다. 전건 규칙군과 후건 규칙군은, 각각 자연 연역 체계의 제거 규칙과 도입 규칙과 밀접한 연관을 갖는다. 이를 가장 쉽게 확인해보는 방법은, 여분공식 \(\Gamma, \Delta\)가 없는 경우를 생각해보는 것이다. \(\wedge_{L1}\)과 \(\wedge_{R}\) 규칙을 각각 상응하는 자연 연역 규칙에 대응시켜 보겠다. \[ \begin{prooftree} \AxiomC{$A\Rightarrow$} \RightLabel{$\wedge_{L1}$} \UnaryInfC{ $A\wedge B\Rightarrow$ } \end{prooftree} \mkern4em\begin{prooftree} \AxiomC{$\uparrow A\wedge B$} \RightLabel{$\wedge^{-}$} \UnaryInfC{ $\uparrow A$ } \end{prooftree} \]

\[ \begin{prooftree} \AxiomC{ $\Rightarrow A$ } \AxiomC{ $\Rightarrow B$ } \RightLabel{ $\wedge_{R}$ } \BinaryInfC{ $\Rightarrow (A\wedge B)$ } \end{prooftree} \kern4em \begin{prooftree} \AxiomC{ $\downarrow A$ } \AxiomC{ $\downarrow B$ } \RightLabel{ $\wedge^{+}$ } \BinaryInfC{ $\downarrow A\wedge B$ } \end{prooftree} \]

\(\wedge_{L1}\) 규칙은 전건에 \(A\wedge B\)를 도입한다. 이는 자연 연역 증명에서는 \(A\)로부터 상향 탐색하기 위해 \(\wedge\) 제거 규칙이 사용된 경우 \(A\wedge B\)를 상향 탐색해야 함을 의미한다. 반면 \(\wedge_{R}\) 규칙의 경우 자연 연역의 도입 규칙에 대응하는데, \(A\)와 \(B\)를 결론으로 갖는 증명 트리로부터 하향 탐색할 때 \(\wedge\) 도입 규칙이 사용되면 \(A\wedge B\) 라벨 노드를 하향 생성함을 지시한다. 즉, 시퀀트의 전건 규칙은 자연 연역에서 상향 탐색에 대응되고, 후건 규칙은 자연 연역의 하향 탐색에 대응된다.

보론: 구조 규칙의 우위

상단의 구조 규칙은 람벡(J. Lambek)의 범주문법(categorical grammar)과 지라르(J.-Y. Girard)의 선형 논리(linear logic) 등에서는 부정된다. 이처럼, 시퀀트 계산 체계를 올바르게 정의했을 때, 구조 규칙이 일반적으로 성립하지 않는 논리군을 부분구조논리(substructural logic, \(\textbf{SL}\))라 부른다. 오늘날 구조 규칙의 종류는 \(W, C, E\)뿐만 아니라 더 세분화되었다.

• 왼쪽 약화는 연언 중립원(neutral/identity constant) \(\textbf{t}/\overline{1}\) (또는, 경우에 따라 \(\textbf{T}/\top\))의 성질을 결정한다. 오른쪽 약화는 선언 중립원 \(\textbf{f}/\overline{0}\) (마찬가지로 또는 \(\textbf{F}/\bot\))의 성질을 결정한다. 따라서 왼쪽 약화와 오른쪽 약화를 나누어 각각 \(i\), \(o\)로 부르기도 한다.
• 축약 규칙에서도 엄격하게 \(C_{L}\)만을 축약(\(c\))이라 부르면서, \(C_R\)또는 그 듀얼을 밍글(mingle)이나 확장(expansion, \(p\))으로 나누어 부르는 경우가 있다. 특히 연관 논리의 경우, 약화는 성립하지 않지만 축약은 성립하므로, 성립하는 축약의 종류와 강도에 따라 축약 규칙을 세분화한다.
• 교환 규칙(\(e\))도 치환(permutation)이나 가환(commutativity)으로 부르는 경우도 있다.
• \(W, C, E\) 규칙이 모두 제거된 경우를 완전람벡논리(Full Lambek Logic, \(\textbf{FL}\))라 부른다. 반면 위 시퀀트 계산으로는 표현할 수 없는 규칙도 있다. 시퀀트는 전건과 후건이 문장의 나열임을 전제하고, 나열의 병합 조작은 결합법칙이 성립한다. (모노이드를 형성한다.) 그러나 결합법칙 구조규칙 \(a\) 또한 제거될 수 있다. 이런 체계들도 부분구조논리지만, 완전람벡논리는 아니다. 역으로, 무제약 부분구조논리 \(\textbf{SL}\)에 결합법칙 \(a\) 조건을 추가한 체계(\(\textbf{SL}_a\))를 완전람벡논리로 볼 수 있다.
• \(e, a, c, p, i, o\) 구조 규칙은 모두 서로 독립적이다.

시스템 \(\textbf{LJ}\)

\(\textbf{LJ}\)는 모든 시퀀트의 후건이 단일 문장이라는 점을 빼면 \(\textbf{LK}\)와 동일하다. 그러나 \(\textbf{LJ}\)의 증명 능력은 \(\textbf{LK}\)보다 약하다. 왜냐하면, 후건이 단일 문장이라는 조건 때문에, \(W_{R}\)은 제한적으로만 적용되고, \(C_{R}\)은 아예 적용할 수 없기 때문이다.

시스템 \(\textbf{G}_3\): 비분석적 규칙의 제거, 논리연결사 규칙으로의 매입

(작성중)

참고문헌, 더 읽으면 좋은 글들

겐첸의 원전과 번역본

• Gentzen, G. (1935). Untersuchungen über das logische Schließen: I/II. Mathematische Zeitschrift, 35.
• Gentzen, G. (1964). Investigations into logical deduction (M. Szabo, Trans.). In: The Collected Papers of Gerhard Gentzen.

중요 연구서 및 교과서

• Prawitz, D. (1965). Natural Deudction: A Proof-Theoretical Study.
• Kleene, S. (1952). Introduction to Metamathematics.

\(\textbf{LK}\), \(\textbf{LJ}\)를 다루는 증명론 교과서

출간일이 아닌, 대략적인 난이도 순으로 정렬했다.

• Ono, H. (2019). Proof Theory and Algebra in Logic.
• Takeuti, G. (2013). Proof Theory. Dover ed.
• Pohlers, W. (1989). Proof Theory: An Introduction.
• Troelstra, A. and H. Schwichtenberg. (2000). Basic Proof Theory. 2nd ed.
  • 참고: 트뢸스트라와 슈비히텐베르크의 교재는 (i) 전혀 베이직하지 않으며, (ii) 독학자를 위해 설명이 잘 짜여진 책이라기보다는 교수자가 있을 때 쓸 수 있는 참고서에 가깝다.
• Girard, J.-Y. (1987). Proof Theory and Logical Complexity. Vol. 1.